Nuprl Definition : sendMinimalR 11,40

sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR(Ttlds1ds2PQd1d2f)
== ([weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([weakSendDoApplyR(Ttlds1f o' mu'(s,n(P(s,n)))); 

== ([weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([weakSendDoApplyR(; 0; lnk-inv(l); ds2; mu'(s,n(Q(s,n))))]) 
latex



clarification:

sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR(Ttlds1ds2PQd1d2f)
== ([weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([weakSendDoApplyR(Ttlds1f o' mu'(State(ds1);s,n(P(s,n));d1)) / 
== ([[weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([[weakSendDoApplyR(; 0; lnk-inv(l); ds2; mu'(State(ds2);s,n(Q(s,n));d2)) / 
== ([[[]]]) 
latex


Definitions(L), f o' g, [car / cdr], weakSendDoApplyR{$a:ut2, $tg:ut2}(Ttldsf), , #$n, lnk-inv(l), mu'(P), State(ds), x.A(x), b, f(a), []

origin